Event B (english version)
Identifieur interne : 000A25 ( Main/Exploration ); précédent : 000A24; suivant : 000A26Event B (english version)
Auteurs : Neeraj Kumar Singh [Canada] ; Dominique Méry [France]Source :
English descriptors
Abstract
This chapter provides results on the modeling and verification of systems using transition systems. The goal is to provide the basic fundamental and conceptual theories, which support Event B approach. The chapter explains how invariant properties and safety properties are defined in the framework of a transition system, which may model a program, an algorithm or a distributed system. It details the Event B language and related concepts such as events, contexts, machines and refinement. The chapter explains proof obligations (POs) generated for checking the consistency of the Event B structure. It develops three case studies, in order to illustrate the incremental and proof-based modeling using Event B. The chapter emphasizes the notion of proof-based patterns applied for the Event B method. It describes available tools for supporting the Event B modeling language concludes with the current and future trends for this method.
Url:
DOI: 10.1002/9781119002727.ch10
Affiliations:
Links toward previous steps (curation, corpus...)
- to stream Hal, to step Corpus: 002060
- to stream Hal, to step Curation: 002060
- to stream Hal, to step Checkpoint: 000963
- to stream Main, to step Merge: 000A27
- to stream Main, to step Curation: 000A25
Le document en format XML
<record><TEI><teiHeader><fileDesc><titleStmt><title xml:lang="en">Event B (english version)</title>
<author><name sortKey="Singh, Neeraj Kumar" sort="Singh, Neeraj Kumar" uniqKey="Singh N" first="Neeraj Kumar" last="Singh">Neeraj Kumar Singh</name>
<affiliation wicri:level="1"><hal:affiliation type="laboratory" xml:id="struct-240631" status="INCOMING"><orgName>McMaster University</orgName>
<desc><address><addrLine>Hamilton, Ontario</addrLine>
<country key="CA"></country>
</address>
</desc>
<listRelation><relation active="#struct-357717" type="direct"></relation>
</listRelation>
<tutelles><tutelle active="#struct-357717" type="direct"><org type="institution" xml:id="struct-357717" status="INCOMING"><orgName>McMaster Centre For Software Certification</orgName>
<desc><address><country key="FR"></country>
</address>
</desc>
</org>
</tutelle>
</tutelles>
</hal:affiliation>
<country>Canada</country>
</affiliation>
</author>
<author><name sortKey="Mery, Dominique" sort="Mery, Dominique" uniqKey="Mery D" first="Dominique" last="Méry">Dominique Méry</name>
<affiliation wicri:level="1"><hal:affiliation type="laboratory" xml:id="struct-206040" status="VALID"><idno type="IdRef">067077927</idno>
<idno type="RNSR">198912571S</idno>
<idno type="IdUnivLorraine">[UL]RSI--</idno>
<orgName>Laboratoire Lorrain de Recherche en Informatique et ses Applications</orgName>
<orgName type="acronym">LORIA</orgName>
<date type="start">2012-01-01</date>
<desc><address><addrLine>Campus Scientifique BP 239 54506 Vandoeuvre-lès-Nancy Cedex</addrLine>
<country key="FR"></country>
</address>
<ref type="url">http://www.loria.fr</ref>
</desc>
<listRelation><relation active="#struct-300009" type="direct"></relation>
<relation active="#struct-413289" type="direct"></relation>
<relation name="UMR7503" active="#struct-441569" type="direct"></relation>
</listRelation>
<tutelles><tutelle active="#struct-300009" type="direct"><org type="institution" xml:id="struct-300009" status="VALID"><orgName>Institut National de Recherche en Informatique et en Automatique</orgName>
<orgName type="acronym">Inria</orgName>
<desc><address><addrLine>Domaine de VoluceauRocquencourt - BP 10578153 Le Chesnay Cedex</addrLine>
<country key="FR"></country>
</address>
<ref type="url">http://www.inria.fr/en/</ref>
</desc>
</org>
</tutelle>
<tutelle active="#struct-413289" type="direct"><org type="institution" xml:id="struct-413289" status="VALID"><idno type="IdRef">157040569</idno>
<idno type="IdUnivLorraine">[UL]100--</idno>
<orgName>Université de Lorraine</orgName>
<orgName type="acronym">UL</orgName>
<date type="start">2012-01-01</date>
<desc><address><addrLine>34 cours Léopold - CS 25233 - 54052 Nancy cedex</addrLine>
<country key="FR"></country>
</address>
<ref type="url">http://www.univ-lorraine.fr/</ref>
</desc>
</org>
</tutelle>
<tutelle name="UMR7503" active="#struct-441569" type="direct"><org type="institution" xml:id="struct-441569" status="VALID"><idno type="ISNI">0000000122597504</idno>
<idno type="IdRef">02636817X</idno>
<orgName>Centre National de la Recherche Scientifique</orgName>
<orgName type="acronym">CNRS</orgName>
<date type="start">1939-10-19</date>
<desc><address><country key="FR"></country>
</address>
<ref type="url">http://www.cnrs.fr/</ref>
</desc>
</org>
</tutelle>
</tutelles>
</hal:affiliation>
<country>France</country>
<placeName><settlement type="city">Nancy</settlement>
<settlement type="city">Metz</settlement>
<region type="region" nuts="2">Grand Est</region>
<region type="old region" nuts="2">Lorraine (région)</region>
</placeName>
<orgName type="university">Université de Lorraine</orgName>
</affiliation>
</author>
</titleStmt>
<publicationStmt><idno type="wicri:source">HAL</idno>
<idno type="RBID">Hal:hal-01216779</idno>
<idno type="halId">hal-01216779</idno>
<idno type="halUri">https://hal.inria.fr/hal-01216779</idno>
<idno type="url">https://hal.inria.fr/hal-01216779</idno>
<idno type="doi">10.1002/9781119002727.ch10</idno>
<date when="2014-07-22">2014-07-22</date>
<idno type="wicri:Area/Hal/Corpus">002060</idno>
<idno type="wicri:Area/Hal/Curation">002060</idno>
<idno type="wicri:Area/Hal/Checkpoint">000963</idno>
<idno type="wicri:explorRef" wicri:stream="Hal" wicri:step="Checkpoint">000963</idno>
<idno type="wicri:Area/Main/Merge">000A27</idno>
<idno type="wicri:Area/Main/Curation">000A25</idno>
<idno type="wicri:Area/Main/Exploration">000A25</idno>
</publicationStmt>
<sourceDesc><biblStruct><analytic><title xml:lang="en">Event B (english version)</title>
<author><name sortKey="Singh, Neeraj Kumar" sort="Singh, Neeraj Kumar" uniqKey="Singh N" first="Neeraj Kumar" last="Singh">Neeraj Kumar Singh</name>
<affiliation wicri:level="1"><hal:affiliation type="laboratory" xml:id="struct-240631" status="INCOMING"><orgName>McMaster University</orgName>
<desc><address><addrLine>Hamilton, Ontario</addrLine>
<country key="CA"></country>
</address>
</desc>
<listRelation><relation active="#struct-357717" type="direct"></relation>
</listRelation>
<tutelles><tutelle active="#struct-357717" type="direct"><org type="institution" xml:id="struct-357717" status="INCOMING"><orgName>McMaster Centre For Software Certification</orgName>
<desc><address><country key="FR"></country>
</address>
</desc>
</org>
</tutelle>
</tutelles>
</hal:affiliation>
<country>Canada</country>
</affiliation>
</author>
<author><name sortKey="Mery, Dominique" sort="Mery, Dominique" uniqKey="Mery D" first="Dominique" last="Méry">Dominique Méry</name>
<affiliation wicri:level="1"><hal:affiliation type="laboratory" xml:id="struct-206040" status="VALID"><idno type="IdRef">067077927</idno>
<idno type="RNSR">198912571S</idno>
<idno type="IdUnivLorraine">[UL]RSI--</idno>
<orgName>Laboratoire Lorrain de Recherche en Informatique et ses Applications</orgName>
<orgName type="acronym">LORIA</orgName>
<date type="start">2012-01-01</date>
<desc><address><addrLine>Campus Scientifique BP 239 54506 Vandoeuvre-lès-Nancy Cedex</addrLine>
<country key="FR"></country>
</address>
<ref type="url">http://www.loria.fr</ref>
</desc>
<listRelation><relation active="#struct-300009" type="direct"></relation>
<relation active="#struct-413289" type="direct"></relation>
<relation name="UMR7503" active="#struct-441569" type="direct"></relation>
</listRelation>
<tutelles><tutelle active="#struct-300009" type="direct"><org type="institution" xml:id="struct-300009" status="VALID"><orgName>Institut National de Recherche en Informatique et en Automatique</orgName>
<orgName type="acronym">Inria</orgName>
<desc><address><addrLine>Domaine de VoluceauRocquencourt - BP 10578153 Le Chesnay Cedex</addrLine>
<country key="FR"></country>
</address>
<ref type="url">http://www.inria.fr/en/</ref>
</desc>
</org>
</tutelle>
<tutelle active="#struct-413289" type="direct"><org type="institution" xml:id="struct-413289" status="VALID"><idno type="IdRef">157040569</idno>
<idno type="IdUnivLorraine">[UL]100--</idno>
<orgName>Université de Lorraine</orgName>
<orgName type="acronym">UL</orgName>
<date type="start">2012-01-01</date>
<desc><address><addrLine>34 cours Léopold - CS 25233 - 54052 Nancy cedex</addrLine>
<country key="FR"></country>
</address>
<ref type="url">http://www.univ-lorraine.fr/</ref>
</desc>
</org>
</tutelle>
<tutelle name="UMR7503" active="#struct-441569" type="direct"><org type="institution" xml:id="struct-441569" status="VALID"><idno type="ISNI">0000000122597504</idno>
<idno type="IdRef">02636817X</idno>
<orgName>Centre National de la Recherche Scientifique</orgName>
<orgName type="acronym">CNRS</orgName>
<date type="start">1939-10-19</date>
<desc><address><country key="FR"></country>
</address>
<ref type="url">http://www.cnrs.fr/</ref>
</desc>
</org>
</tutelle>
</tutelles>
</hal:affiliation>
<country>France</country>
<placeName><settlement type="city">Nancy</settlement>
<settlement type="city">Metz</settlement>
<region type="region" nuts="2">Grand Est</region>
<region type="old region" nuts="2">Lorraine (région)</region>
</placeName>
<orgName type="university">Université de Lorraine</orgName>
</affiliation>
</author>
</analytic>
<idno type="DOI">10.1002/9781119002727.ch10</idno>
</biblStruct>
</sourceDesc>
</fileDesc>
<profileDesc><textClass><keywords scheme="mix" xml:lang="en"><term>Event B</term>
<term>proof obligations (POs)</term>
<term>transition system</term>
</keywords>
</textClass>
</profileDesc>
</teiHeader>
<front><div type="abstract" xml:lang="en">This chapter provides results on the modeling and verification of systems using transition systems. The goal is to provide the basic fundamental and conceptual theories, which support Event B approach. The chapter explains how invariant properties and safety properties are defined in the framework of a transition system, which may model a program, an algorithm or a distributed system. It details the Event B language and related concepts such as events, contexts, machines and refinement. The chapter explains proof obligations (POs) generated for checking the consistency of the Event B structure. It develops three case studies, in order to illustrate the incremental and proof-based modeling using Event B. The chapter emphasizes the notion of proof-based patterns applied for the Event B method. It describes available tools for supporting the Event B modeling language concludes with the current and future trends for this method.</div>
</front>
</TEI>
<affiliations><list><country><li>Canada</li>
<li>France</li>
</country>
<region><li>Grand Est</li>
<li>Lorraine (région)</li>
</region>
<settlement><li>Metz</li>
<li>Nancy</li>
</settlement>
<orgName><li>Université de Lorraine</li>
</orgName>
</list>
<tree><country name="Canada"><noRegion><name sortKey="Singh, Neeraj Kumar" sort="Singh, Neeraj Kumar" uniqKey="Singh N" first="Neeraj Kumar" last="Singh">Neeraj Kumar Singh</name>
</noRegion>
</country>
<country name="France"><region name="Grand Est"><name sortKey="Mery, Dominique" sort="Mery, Dominique" uniqKey="Mery D" first="Dominique" last="Méry">Dominique Méry</name>
</region>
</country>
</tree>
</affiliations>
</record>
Pour manipuler ce document sous Unix (Dilib)
EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/Main/Exploration
HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 000A25 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Main/Exploration/biblio.hfd -nk 000A25 | SxmlIndent | more
Pour mettre un lien sur cette page dans le réseau Wicri
{{Explor lien |wiki= Wicri/Lorraine |area= InforLorV4 |flux= Main |étape= Exploration |type= RBID |clé= Hal:hal-01216779 |texte= Event B (english version) }}
This area was generated with Dilib version V0.6.33. |